!pip  -q install --upgrade pyprover9
import pyprover9

ASSUMPTIONS = """

    % SORT AXIOMS: Establish two sorts.
    all x (Entity(x) | World(x)).
    all x -(Entity(x) & World(x)).
    all w all v (A(w,v) -> World(w) & World(v)).
    all a all w (In(a,w) -> Entity(a) & World(w)).

    % AXIOM (alpha): No world is accessible from an empty world.
    all w all v ((World(w) & World(v) & (all a (Entity(a) -> -In(a,w))) & (exists b (Entity(b) & In(b,v)))) -> -A(w,v)).

    % (1): Every entity is contingent.
    all a ( Entity(a) -> exists w exists v ( World(w) & World(v) & -In(a,w) & In(a,v) & A(w,v) ) ).
    
"""

GOAL = """
    % (F): Every entity is in a F-relation with some other entity. 
all a ( Entity(a) -> exists b exists w exists v ( Entity(b) & World(w) & World(v) & -In(a,w) & In(b,w) & In(a,v) & A(w,v) ) ).
    

% If "Proved", then: Alpha and (1) entails (F)

"""

pyprover9.prove( ASSUMPTIONS, GOAL)